Summary

• Records the 2026-05-28 investigation finding that Phase B Slice 1 (TEcho linearity wire) is structurally larger than the saved plan implied, and the owner directive to defer until Phase D.
• Reorients `STATE.a2ml` next_action to Phase C — closure of the two list-vs-multiset structural admits at `formal/Semantics_L1.v:553/621` inside `region_shrink_preserves_typing_l1_gen_m`.
• No proof changes — `coqc 8.18.0` clean rebuild verified (9/9 .v files `Qed`).

Background — the Phase B Slice 1 deferral

The original Phase B Slice 1 plan was a one-line definitional refinement: add `| TEcho _ => true` to `is_linear_ty` in `formal/Syntax.v`, realising the design intent annotated at `TypingL1.v:T_Observe_L1`.

Investigation 2026-05-28 revealed the wire's true scope:

• Legacy `Semantics.v` impact: vacuous. `linear_value_is_loc` (Semantics.v:2625) gains a TEcho branch closeable by `inversion Htype; discriminate` because legacy `Typing.v` has zero typing rules producing `TEcho` (grep-verified).
• L1 impact: structurally non-vacuous. At L1, `EEcho T v` is both a value (`VEcho` in Syntax.v:152) AND typed at `TEcho T` (via `T_Echo_L1` in TypingL1.v:351-354). This refutes the conclusion of `linear_value_is_loc_l1` (Semantics_L1.v:891) — the lemma claims "linear-typed value ⇒ `ELoc` with `TString r`", but `EEcho T v` is a linear-typed value that is neither. The lemma feeds 9 call-sites inside `subst_typing_gen_l1_m` (Semantics_L1.v:1326-1605, `Qed`), which is foundational L1 substitution scaffolding for `preservation_l1`.

Three resolution paths were surfaced (`AskUserQuestion` 2026-05-28):

1. Disjunctive rewrite + 9-caller updates: structurally correct but adds ~9 forward-looking `Admitted` sites to the L1 substitution chain.
2. Layered predicate split: introduce `is_linear_ty_l3` keeping legacy `is_linear_ty` alone. Zero legacy touch but adds definitional duplication.
3. Defer until Phase D: Phase D (L2 effect-typed `TFun`) will reshape the L1 substitution chain anyway. The wire lands naturally once that infrastructure exists.

Owner chose (3) defer — Phase D will create the right shape for the wire to land cleanly without the disjunctive rewrite.

Phase C scoping (this commit)

`STATE.a2ml` next_action now reads: "Phase C — L1 structural list-vs-multiset bridge (1-2 PRs). Closes `Semantics_L1.v` structural admits at ~line 553/621 + 1 outer `Admitted` that depend on them. Bridge predicate choice (rotation vs permutation vs abstract multiset) is the first design decision. Branch: `proof/phase-c-l1-multiset-bridge`."

Mapping verified:

• Lines 553 + 621: both inside `region_shrink_preserves_typing_l1_gen_m`, T_Region_Active_L1 `rr = r` shadowed case + T_Region_Active_L1_Echo mirror. Phase C scope.
• Lines 1256 + 1276: in `region_liveness_at_split_l1_gen`, "GENUINELY FALSE at L1" per source comment at 1253 — closes naturally at Phase D's L2 effect-typed TFun. NOT Phase C scope.
• Line 1694: lambda-rigidity admit inside `preservation_l1`'s outer Admitted. Phase D scope.

Closure of 553 + 621 ⇒ outer `Admitted` at line 653 (`region_shrink_preserves_typing_l1_gen_m`) flips to `Qed`. That makes the value-restricted wrapper at line 666-676 (`region_shrink_preserves_typing_l1`) actually-`Qed` (currently `Qed` only under the outer `Admitted`).

Test plan

• `coqc 8.18.0` clean rebuild — all 9 .v files `Qed`
• No proof changes; only PROOF-NEEDS.md row + STATE.a2ml refresh
• CI: standard governance + scorecard

🤖 Generated with Claude Code